<html>
<head><meta charset="utf-8"><title>meaning of &quot;invariant&quot; · general · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/index.html">general</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html">meaning of &quot;invariant&quot;</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="148053515"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148053515" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148053515">(Nov 20 2018 at 17:10)</a>:</h4>
<blockquote>
<p>not clear what this method's invariants are - i.e. when is the unsafe code actually not UB</p>
</blockquote>
<p>I feel like this isn't a proper <em>English</em> use of the word "invariant", but it seems consistent in the compiler circles. What does "invariant" mean when it doesn't mean "something that doesn't change"? </p>
<p>/cc <span class="user-mention" data-user-id="119009">@eddyb</span></p>



<a name="148053555"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148053555" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> eddyb <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148053555">(Nov 20 2018 at 17:11)</a>:</h4>
<p><del>it means precondition</del>. it's always true (in the absence of UB), making it an invariant :P</p>



<a name="148053560"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148053560" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> eddyb <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148053560">(Nov 20 2018 at 17:11)</a>:</h4>
<p>maybe a stretch but I think it makes sense on some level</p>



<a name="148053628"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148053628" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> QuietMisdreavus <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148053628">(Nov 20 2018 at 17:12)</a>:</h4>
<p>sometimes in computing an "invariant" is something you can assume to be true at all times, or at least throughout a given function/module/scope/etc</p>



<a name="148053687"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148053687" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> eddyb <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148053687">(Nov 20 2018 at 17:13)</a>:</h4>
<p>that's more eloquent than what I said, but I agree, that's how I see it as well :D</p>



<a name="148053851"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148053851" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148053851">(Nov 20 2018 at 17:16)</a>:</h4>
<p>invariant != precondition</p>



<a name="148053864"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148053864" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148053864">(Nov 20 2018 at 17:16)</a>:</h4>
<p>so I think "method's precondition" would be a better term here</p>



<a name="148053874"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148053874" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> eddyb <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148053874">(Nov 20 2018 at 17:16)</a>:</h4>
<p>words are hard :(</p>



<a name="148053898"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148053898" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148053898">(Nov 20 2018 at 17:17)</a>:</h4>
<p>true^^</p>



<a name="148053904"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148053904" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148053904">(Nov 20 2018 at 17:17)</a>:</h4>
<p>to call it an invariant, you should <em>at least</em> have it both as pre- and postcondition</p>



<a name="148053960"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148053960" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148053960">(Nov 20 2018 at 17:18)</a>:</h4>
<p>that's still stretching the term IMO, I assoicate invariants with something that several threads can rely on and that can be shared because it is true forever, but that may be just my niche^^</p>



<a name="148054238"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148054238" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148054238">(Nov 20 2018 at 17:23)</a>:</h4>
<p>I think the combination of all this was useful, thank you.</p>



<a name="148054315"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148054315" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148054315">(Nov 20 2018 at 17:24)</a>:</h4>
<p>It feels like if something is an invariant, you wouldn't actually perform a check for it, whereas I feel like pre/post conditions are actual checks in the code</p>



<a name="148054342"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148054342" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148054342">(Nov 20 2018 at 17:25)</a>:</h4>
<p>e.g. an invariant of <code>&amp;str</code> is that it's UTF-8. I might use a pre/post condition to enforce that at some boundary</p>



<a name="148054353"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148054353" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148054353">(Nov 20 2018 at 17:25)</a>:</h4>
<p>and if I fail to enforce an invariant, then I might open myself up to UB</p>



<a name="148054767"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148054767" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> QuietMisdreavus <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148054767">(Nov 20 2018 at 17:32)</a>:</h4>
<p>yeah, violation of invariants is where you start getting into awkward bugs, UB, etc</p>



<a name="148057537"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148057537" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148057537">(Nov 20 2018 at 18:26)</a>:</h4>
<p>There is <em>one</em> particular invariant violating which is instantenous UB, the "validity invariant" as I call it</p>



<a name="148057549"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148057549" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148057549">(Nov 20 2018 at 18:26)</a>:</h4>
<p>that's because the compiler knows about it</p>



<a name="148057572"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148057572" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148057572">(Nov 20 2018 at 18:27)</a>:</h4>
<p>violating, for example, the loop invariant of your quicksort won't give you UB. So I wouldnt connect invariants and UB directly at all</p>



<a name="148057575"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148057575" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148057575">(Nov 20 2018 at 18:27)</a>:</h4>
<p>invariants are just both useful for specification and for verification of programs</p>



<a name="148057780"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148057780" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148057780">(Nov 20 2018 at 18:30)</a>:</h4>
<p>right, which is why I said "<em>might</em> open myself up to UB"</p>



<a name="148058274"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148058274" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148058274">(Nov 20 2018 at 18:38)</a>:</h4>
<p>one thing to keep in mind is that all invariants, preconditions, postconditions, proof obligations, etc. are in service of a particular goal. e.g. the quicksort loop invariant is for the functional correctness of the sorting, while in rust development we typically implicitly refer to memory safety (or a particular aspect of it) as the goal. mixing these unstated contexts tends to cause confusion</p>



<a name="148058607"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148058607" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148058607">(Nov 20 2018 at 18:44)</a>:</h4>
<blockquote>
<p>unstated contexts tends to cause confusion</p>
</blockquote>
<p>Sounds true in every case <span class="emoji emoji-1f638" title="smile cat">:smile_cat:</span></p>



<a name="148059020"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/meaning%20of%20%22invariant%22/near/148059020" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/meaning.20of.20.22invariant.22.html#148059020">(Nov 20 2018 at 18:51)</a>:</h4>
<p>we also often rely on functional correctness for memory safety, so these contexts aren't even all that separate^^</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>